-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(measure_theory/constructions/{pi,prod}): drop some measurability assumptions #10241
Conversation
This is great, and simplifies a lot! |
Looks great. Very nifty proof. I'm still not quite sure I understand why we use bors d+ |
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Oh, linting just succeeded. bors merge |
bors r+ |
… assumptions (#10241) Some lemmas (most notably `prod_prod` and `pi_pi`) are true for non-measurable sets as well.
bors r+ |
… assumptions (#10241) Some lemmas (most notably `prod_prod` and `pi_pi`) are true for non-measurable sets as well.
Pull request successfully merged into master. Build succeeded: |
third time's a charm! |
Some lemmas (most notably
prod_prod
andpi_pi
) are true for non-measurable sets as well.